#ifdef KITSCHY_DEBUG_MEMORY 
#include "debug_memorymanager.h"
#endif

#include "stdio.h"
#include "stdlib.h"
#include "string.h"
#include "stdarg.h"
#include "assert.h"

#include "BList.h"

#include "symbol.h"
#include "sort.h"
#include "ontology.h"
#include "featureterm.h"
#include "FTKBase.h"
#include "FT_refinement.h"
#include "Ufeatureterm.h"

#include "SpecialTerm.h"


FeatureTerm *simple_unification(FeatureTerm *f1,FeatureTerm *f2,Ontology *ontology,FTKBase *domain_model)
{
	List<FeatureTerm> *results = unification(f1,f2,ontology,domain_model);
	FeatureTerm *result = 0;

	if (results!=0) {
		if (results->Length()>0) result = results->ExtractIni();
		delete results;
	} // if 

	return result;
} /* simple_unification */ 


List<FeatureTerm> *unification(FeatureTerm *f1,FeatureTerm *f2,Ontology *ontology,FTKBase *domain_model)
{
	List<UnificationResult> *l;
	List<FeatureTerm> *result=0;
	List<UnificationBinding> *bindings=new List<UnificationBinding>;
	List<FeatureTerm> *stack=new List<FeatureTerm>;

	l=ft_internal_unification(f1,f2,bindings,stack,ontology,domain_model);

	if (l!=0 && !l->EmptyP()) {
		UnificationResult *r;
		result=new List<FeatureTerm>;
		while(!l->EmptyP()) {
			r=l->ExtractIni();
			result->Add(new FeatureTerm(r->m_u));
			delete r;
		} /* while */ 
	} /* if */ 

	delete bindings;
	delete stack;

	if (l!=0) delete l;

	return result;
} // unification


List<UnificationResult> *unification_with_bindings(FeatureTerm *f1,FeatureTerm *f2,Ontology *ontology,FTKBase *domain_model)
{
	List<UnificationResult> *l;
	List<FeatureTerm> *result=0;
	List<UnificationBinding> *bindings=new List<UnificationBinding>;
	List<FeatureTerm> *stack=new List<FeatureTerm>;

	l=ft_internal_unification(f1,f2,bindings,stack,ontology,domain_model);

	delete bindings;
	delete stack;

	return l;
} /* unification_with_bindings */ 



List<UnificationResult> *ft_internal_unification(FeatureTerm *f1,FeatureTerm *f2,List<UnificationBinding> *bindings,List<FeatureTerm> *stack,Ontology *ontology,FTKBase *domain_model)
{
	List<UnificationResult> *lr;
	UnificationResult *r,*r2;
	FeatureTerm *u=0;
/*
	printf("\n<%i> [ ",stack->Length());
	{
		int i;
		for(i=0;i<stack->Length();i++) printf("%i ",stack->operator [](i)->getDataType());
	}
	printf("]");

	printf("<ft_internal_unification(%p,%p,%i)>\n",f1,f2,bindings->Length());

	{
		char *s;
		if (f1!=0) {
			s=f1->toStringNOOS(domain_model);
			printf("f1:\n%s\n",s);
			delete []s;
		} else {
			printf("f1: -\n");
		} // if 
		if (f2!=0) {
			s=f2->toStringNOOS(domain_model);
			printf("f2:\n%s\n",s);
			delete []s;
		} else {
			printf("f2: -\n");
		} // if 
		printf("\n");
	}
*/
	// Check bindings:
	{
		UnificationBinding *b;
		bindings->Rewind();
		while(bindings->Iterate(b)) {
			if ((b->m_f1==0 || !b->m_f1->isSet()) &&
				(b->m_f2==0 || !b->m_f2->isSet())) {
				if (f1!=0 && f2!=0 &&
					b->m_f1!=0 && b->m_f2!=0 && 
					*(b->m_f1)==*(f1) && *(b->m_f2)==*(f2)) {
					lr=new List<UnificationResult>;
					r=new UnificationResult();
					r->m_u=new FeatureTerm(b->m_u);
					r->m_bindings.Copy(*bindings);
					r->m_stack.Copy(*stack);
					lr->Add(r);

	//				printf("<ft_internal_unification succeeded[BF] and returned %i results>\n",lr->Length());
					return lr;
				} /* if */ 

	//			if (f1!=0 && b->m_f1!=0 && *(b->m_f1)==*(f1)) {
				if (f1!=0 && b->m_f1!=0 && b->m_f1->same(f1)) {
					if (f2==0 || f2->subsumes(b->m_u)) {
						lr=new List<UnificationResult>;
						r=new UnificationResult();
						r->m_u=new FeatureTerm(b->m_u);
						r->m_bindings.Copy(*bindings);
						r->m_bindings.Add(new UnificationBinding(f1,f2,b->m_u));
						r->m_stack.Copy(*stack);
						lr->Add(r);

	//					printf("<ft_internal_unification succeeded[B<f1>F] and returned %i results>\n",lr->Length());
						return lr;
					} else {
	//					printf("<ft_internal_unification found a binding<f1>, but it requires further refinement...>\n");
						{
							int pos=bindings->PositionRef(b);
							UnificationBinding *b2;
							FeatureTerm *old_ft,*new_ft;

							if (*(b->m_u)==*(f1)) return 0;
							lr=ft_internal_unification(b->m_u,f2,bindings,stack,ontology,domain_model);
							if (lr==0) return 0;

							lr->Rewind();
							while(lr->Iterate(r)) {
								b2=r->m_bindings[pos];
								old_ft=b2->m_u;
								new_ft=r->m_u;
	/*
								printf("<------------------------------->\n");
								printf("Now I should substitute all the appearances of:\n");
								char *s=old_ft->toStringNOOS(domain_model);
								printf("%s\n",s);
								delete []s;
								printf("by:\n");
								s=new_ft->toStringNOOS(domain_model);
								printf("%s\n",s);
								delete []s;
								printf("...\n");
								printf("<------------------------------->\n");
	*/
								r->substitute(old_ft,new_ft);
								
							} /* while */ 

							return lr;
						}
					} // if 
				} // if 
	//			if (f2!=0 && b->m_f2!=0 && *(b->m_f2)==*(f2)) {
				if (f2!=0 && b->m_f2!=0 && b->m_f2->same(f2)) {
					if (f1==0 || f1->subsumes(b->m_u)) {
						lr=new List<UnificationResult>;
						r=new UnificationResult();
						r->m_u=new FeatureTerm(b->m_u);
						r->m_bindings.Copy(*bindings);
						r->m_bindings.Add(new UnificationBinding(f1,f2,b->m_u));
						r->m_stack.Copy(*stack);
						lr->Add(r);

	//					printf("<ft_internal_unification succeeded[B<f2>F] and returned %i results>\n",lr->Length());
						return lr;
					} else {
	//					printf("<ft_internal_unification found a binding<f2>, but it requires further refinement...>\n");
						{
							int pos=bindings->PositionRef(b);
							UnificationBinding *b2;
							FeatureTerm *old_ft,*new_ft;

							if (*(b->m_u)==*(f2)) return 0;
							lr=ft_internal_unification(f1,b->m_u,bindings,stack,ontology,domain_model);
							if (lr==0) return 0;

							lr->Rewind();
							while(lr->Iterate(r)) {
								b2=r->m_bindings[pos];
								old_ft=b2->m_u;
								new_ft=r->m_u;
	/*
								printf("<------------------------------->\n");
								printf("Now I should substitute all the appearances of:\n");
								char *s=old_ft->toStringNOOS(domain_model);
								printf("%s\n",s);
								delete []s;
								printf("by:\n");
								s=new_ft->toStringNOOS(domain_model);
								printf("%s\n",s);
								delete []s;
								printf("...\n");
								printf("<------------------------------->\n");
	*/
								r->substitute(old_ft,new_ft);
								
							} /* while */ 

							return lr;
						}
					} // if 
				} // if 
			} // if 
		} // while  
	}

	{
		Sort *s=0;

		if (f1!=0 && f1->getSort()->get_data_type()==DATATYPE_SPECIAL) {
			List<FeatureTerm> *l;
			l=f1->getSpecialTerm()->unification(f2,ontology,domain_model);
			if (l==0) return 0;
			lr=new List<UnificationResult>;

			while(!l->EmptyP()) {
				u=l->ExtractIni();
				r=new UnificationResult();
				r->m_u=u;
				r->m_bindings.Copy(*bindings);
				r->m_bindings.Add(new UnificationBinding(f1,f2,u));
				r->m_stack.Copy(*stack);
				lr->Add(r);
			} // while 
			delete l;
			return lr;
		} // if 
		if (f2!=0 && f2->getSort()->get_data_type()==DATATYPE_SPECIAL) {
			List<FeatureTerm> *l;
			l=f2->getSpecialTerm()->unification(f1,ontology,domain_model);
			if (l==0) return 0;
			lr=new List<UnificationResult>;

			while(!l->EmptyP()) {
				u=l->ExtractIni();
				r=new UnificationResult();
				r->m_u=u;
				r->m_bindings.Copy(*bindings);
				r->m_bindings.Add(new UnificationBinding(f1,f2,u));
				r->m_stack.Copy(*stack);
				lr->Add(r);
			} // while 
			delete l;
			return lr;
		} // if 

		if (f1==0) s=f2->getSort();
		if (f2==0) s=f1->getSort();
		if (s==0) s=f1->getSort()->Unification(f2->getSort());
		
		if (s!=0) {
//			printf("Unification sort will be: %s\n",s->get());

			u=new FeatureTerm((Symbol *)0,s,0);

			if (f1->getName()!=0 || f2->getName()!=0) {
				if (f1->getName()!=0 && f2->getName()!=0) {
					if (f1->getName()->cmp(f2->getName())) {
						u->setName(new Symbol(f1->getName()));
					} else {
						delete u;
						u = 0;
					} // if
				} else {
					if (f1->getName()!=0) {
						u->setName(new Symbol(f1->getName()));
					} else {
						u->setName(new Symbol(f2->getName()));
					} // if
				} // if
			} // if

			if (u!=0) {
				if (u->isInt()) {
					u=integer_unification(f1,f2,u,ontology);
					if (u!=0) {
						lr=new List<UnificationResult>;
						r=new UnificationResult();
						r->m_u=new FeatureTerm(u);
						r->m_bindings.Copy(*bindings);
						r->m_bindings.Add(new UnificationBinding(f1,f2,u));
						r->m_stack.Copy(*stack);
						lr->Add(r);

	//					printf("<ft_internal_unification succeeded and returned %i results>\n",lr->Length());
						return lr;
					} // if 
				} // if 

				if (u->isFloat()) {
					u=float_unification(f1,f2,u,ontology);
					if (u!=0) {
						lr=new List<UnificationResult>;
						r=new UnificationResult();
						r->m_u=u;
						r->m_bindings.Copy(*bindings);
						r->m_bindings.Add(new UnificationBinding(f1,f2,u));
						r->m_stack.Copy(*stack);
						lr->Add(r);

	//					printf("<ft_internal_unification succeeded and returned %i results>\n",lr->Length());
						return lr;
					} // if 
				} // if 

				if (u->isSymbol()) {
					if (f1==0 || f1->getDataType()==-1 || f1->getSymbol()==0) {
						delete u;
						u=f2->clone(domain_model);
						lr=new List<UnificationResult>;
						r=new UnificationResult();
						r->m_u=u;
						r->m_bindings.Copy(*bindings);
						if (f1!=0) r->m_bindings.Add(new UnificationBinding(f1,f2,u));
						r->m_stack.Copy(*stack);
						lr->Add(r);

	//					printf("<ft_internal_unification succeeded (f1 was null or abstract) and returned %i results>\n",lr->Length());
						return lr;
					} // if 
					
					if (f2==0 || f2->getDataType()==-1 || f2->getSymbol()==0) {
						delete u;
						u=f1->clone(domain_model);
						lr=new List<UnificationResult>;
						r=new UnificationResult();
						r->m_u=u;
						r->m_bindings.Copy(*bindings);
						if (f2!=0) r->m_bindings.Add(new UnificationBinding(f1,f2,u));
						r->m_stack.Copy(*stack);
						lr->Add(r);

	//					printf("<ft_internal_unification succeeded (f2 was null or abstract) and returned %i results>\n",lr->Length());
						return lr;
					} // if

					if (f1->getSymbol()->cmp(f2->getSymbol())) {
						delete u;
						u=new FeatureTerm((Symbol *)0,new Symbol(f1->getSymbol()),ontology);
						u->setSort(s);
						lr=new List<UnificationResult>;
						r=new UnificationResult();
						r->m_u=u;
						r->m_bindings.Copy(*bindings);
						r->m_bindings.Add(new UnificationBinding(f1,f2,u));
						r->m_stack.Copy(*stack);
						lr->Add(r);

	//					printf("<ft_internal_unification succeeded and returned %i results>\n",lr->Length());
						return lr;
					} // if 
				} // if 
				
				if (u->isFeatureTerm()) {
					List<UnificationResult> *lr2,*lr3;
					List<Symbol> features;
					Symbol *f;
					int i;

					lr=new List<UnificationResult>;
					r=new UnificationResult();
					r->m_u=new FeatureTerm(u);
					r->m_bindings.Copy(*bindings);
					r->m_bindings.Add(new UnificationBinding(f1,f2,u)); 
					r->m_stack.Copy(*stack);
					r->m_stack.Insert(new FeatureTerm(u));
					lr->Add(r);

					{
						List<Symbol> *l=s->getFeatures();
						Symbol *f;

						while(!l->EmptyP()) {
							f=l->ExtractIni();
							if ((f1!=0 && f1->featureValueQuick(f)!=0) || 
								(f2!=0 && f2->featureValueQuick(f)!=0)) {
								features.Add(f);
							} else {
								delete f;
							} /* if */ 
						} /* while */ 
						delete l;
					}

					features.Rewind();
					while(features.Iterate(f)) {

						lr3=new List<UnificationResult>;
						lr->Rewind();
						i=0;
						while(lr->Iterate(r)) {
	//						printf("Considering feature '%s' (with bindings %i/%i)\n",f->get(),i+1,lr->Length());
							i++;

							lr2=set_internal_unification((f1==0 ? 0:f1->featureValueQuick(f)),
														 (f2==0 ? 0:f2->featureValueQuick(f)),&(r->m_bindings),&(r->m_stack),ontology,domain_model,
														 s->featureSingleton(f));
							if (lr2!=0) {
								while(!lr2->EmptyP()) {
									r2=lr2->ExtractIni();

									// look for the proper clone of "r->m_u":
									{
										FeatureTerm *u2;
										if (r2->m_stack[0]->getDataType()==4) delete r2->m_stack.ExtractIni();
										u2=r2->m_stack[0];

										assert(u2!=0);
										assert(!u2->isSet());
										u2->defineFeatureValue(f,r2->m_u);
										r2->m_u=new FeatureTerm(u2);
									}

									lr3->Add(r2);
								} // while
								delete lr2;
							} /* if */ 
						} /* while */ 
						delete lr;
						lr=lr3;

					} /* while */ 

					if (u!=0) delete u;

					// Filter the results for not having repeated ones:
					{
						List<UnificationResult> to_delete;
						List<UnificationResult> good_ones;

						while(!lr->EmptyP()) {
							r=lr->ExtractIni();
							lr->Rewind();
							while(lr->Iterate(r2)) {
								if (r->m_u->subsumes(r2->m_u)) {
									if (!to_delete.MemberRefP(r2)) to_delete.Add(r2);
								} else {
									if (r2->m_u->subsumes(r->m_u)) if (!to_delete.MemberRefP(r)) to_delete.Add(r);
								} // if 
							} // while 
							if (!to_delete.MemberRefP(r)) good_ones.Add(r);
						} // while  

						while(!good_ones.EmptyP()) lr->Add(good_ones.ExtractIni());
					}

	//				printf("<ft_internal_unification succeeded and returned %i results>\n",lr->Length());
					return lr;
				} // if 

				if (u->isAbstract()) {
					List<Symbol> features;

					lr=new List<UnificationResult>;
					r=new UnificationResult();
					r->m_u=new FeatureTerm(u);
					r->m_bindings.Copy(*bindings);
					r->m_bindings.Add(new UnificationBinding(f1,f2,u)); 
					r->m_stack.Copy(*stack);
					r->m_stack.Insert(new FeatureTerm(u));
					lr->Add(r);

					if (u!=0) delete u;

	//				printf("<ft_internal_unification [abstract] succeeded and returned %i results>\n",lr->Length());
	//				fflush(0);
					return lr;
				} // if 

			} // if (u!=0)

			if (u!=0) delete u;
		} // if 
	} 

	return 0;
} // ft_internal_unification


List<UnificationResult> *set_internal_unification(FeatureTerm *f1,FeatureTerm *f2,List<UnificationBinding> *bindings,List<FeatureTerm> *stack,Ontology *ontology,FTKBase *domain_model,bool singleton)
{
	int i,j;
	int size;
	List<FeatureTerm> v1,v2;
	int *assignments1,*assignments2;
	int *assignments2b;
	int max_size=0;

	List<UnificationResult> *initial_lr,*lr,*lr2,*lr3,*final_lr;
	UnificationResult *r,*r2;
	List<Symbol> features;
//	Symbol *f;
/*
	printf("<%i> [ ",stack->Length());
	{
		int i;
		for(i=0;i<stack->Length();i++) printf("%i ",stack->operator [](i)->getDataType());
	}
	printf("]");

	printf("<set_internal_unification(%p,%p,%i)>\n",f1,f2,bindings->Length());
	{
		char *s;
		if (f1!=0) {
			s=f1->toStringNOOS(domain_model);
			printf("f1:\n%s\n",s);
			delete []s;
		} else {
			printf("f1: -\n");
		} // if 
		if (f2!=0) {
			s=f2->toStringNOOS(domain_model);
			printf("f2:\n%s\n",s);
			delete []s;
		} else {
			printf("f2: -\n");
		} // if 
		printf("\n");
	}
*/

	// Check bindings:
	{
		UnificationBinding *b;
		bindings->Rewind();
		while(bindings->Iterate(b)) {
			if (f1!=0 && f2!=0 &&
				b->m_f1!=0 && b->m_f2!=0 && 
				*(b->m_f1)==*(f1) && *(b->m_f2)==*(f2)) {
				lr=new List<UnificationResult>;
				r=new UnificationResult();
				r->m_u=new FeatureTerm(b->m_u);
				r->m_bindings.Copy(*bindings);
				r->m_stack.Copy(*stack);
				lr->Add(r);

//				printf("<set_internal_unification succeeded[BF] and returned %i results>\n",lr->Length());
				return lr;
			} /* if */ 

			if (f1!=0 && b->m_f1!=0 && b->m_f1->isSet() && b->m_f1->same(f1)) {
				if (f2==0 || f2->subsumes(b->m_u)) {
					lr=new List<UnificationResult>;
					r=new UnificationResult();
					r->m_u=new FeatureTerm(b->m_u);
					r->m_bindings.Copy(*bindings);
					r->m_bindings.Add(new UnificationBinding(f1,f2,b->m_u));
					r->m_stack.Copy(*stack);
					lr->Add(r);

//					printf("<set_internal_unification succeeded[B<f1>F] and returned %i results>\n",lr->Length());
					return lr;
				} else {
//					printf("<set_internal_unification found a binding<f1>, but it requires further refinement...>\n");
					{
						int pos=bindings->PositionRef(b);
						UnificationBinding *b2;
						FeatureTerm *old_ft,*new_ft;

						if (*(b->m_u)==*(f1)) return 0;
						lr=set_internal_unification(b->m_u,f2,bindings,stack,ontology,domain_model,singleton);
						if (lr==0) return 0;

						lr->Rewind();
						while(lr->Iterate(r)) {
							b2=r->m_bindings[pos];
							old_ft=b2->m_u;
							new_ft=r->m_u;
/*
							printf("<------------------------------->\n");
							printf("Now I should substitute all the appearances of:\n");
							char *s=old_ft->toStringNOOS(domain_model);
							printf("%s\n",s);
							delete []s;
							printf("by:\n");
							s=new_ft->toStringNOOS(domain_model);
							printf("%s\n",s);
							delete []s;
							printf("...\n");
							printf("<------------------------------->\n");
*/
							r->substitute(old_ft,new_ft);
							
						} /* while */ 

						return lr;
					}
				} // if 
			} // if 
			if (f2!=0 && b->m_f2!=0 && b->m_f2->isSet() && b->m_f2->same(f2)) {
				if (f1==0 || f1->subsumes(b->m_u)) {
					lr=new List<UnificationResult>;
					r=new UnificationResult();
					r->m_u=new FeatureTerm(b->m_u);
					r->m_bindings.Copy(*bindings);
					r->m_bindings.Add(new UnificationBinding(f1,f2,b->m_u));
					r->m_stack.Copy(*stack);
					lr->Add(r);

//					printf("<set_internal_unification succeeded[B<f2>F] and returned %i results>\n",lr->Length());
					return lr;
				} else {
//					printf("<set_internal_unification found a binding<f2>, but it requires further refinement...>\n");
					{
						int pos=bindings->PositionRef(b);
						UnificationBinding *b2;
						FeatureTerm *old_ft,*new_ft;

						if (*(b->m_u)==*(f2)) return 0;
						lr=set_internal_unification(f1,b->m_u,bindings,stack,ontology,domain_model,singleton);
						if (lr==0) return 0;

						lr->Rewind();
						while(lr->Iterate(r)) {
							b2=r->m_bindings[pos];
							old_ft=b2->m_u;
							new_ft=r->m_u;
/*
							printf("<------------------------------->\n");
							printf("Now I should substitute all the appearances of:\n");
							char *s=old_ft->toStringNOOS(domain_model);
							printf("%s\n",s);
							delete []s;
							printf("by:\n");
							s=new_ft->toStringNOOS(domain_model);
							printf("%s\n",s);
							delete []s;
							printf("...\n");
							printf("<------------------------------->\n");
*/
							r->substitute(old_ft,new_ft);
							
						} /* while */ 

						return lr;
					}
				} // if 
			} // if 
		} // while  
	}

	initial_lr=new List<UnificationResult>;
	final_lr=new List<UnificationResult>;
	r=new UnificationResult();
	r->m_u=FeatureTerm::SetFeatureTerm((Symbol *)0);
	r->m_bindings.Copy(*bindings);
	if ((f1!=0 && f1->isSet()) ||(f2!=0 && f2->isSet())) r->m_bindings.Add(new UnificationBinding(f1,f2,r->m_u));
	r->m_stack.Copy(*stack);
	r->m_stack.Insert(new FeatureTerm(r->m_u));
	initial_lr->Add(r);
	
	if (f1!=0) {
		if (f1->isSet()) {
			FeatureTerm *f;
			List<FeatureTerm> *l=f1->set_values_quick();
			l->Rewind();
			while(l->Iterate(f)) v1.Add(f);
		} else {
			v1.Add(f1);
		} /* if */ 
	} /* if */ 
	if (f2!=0) {
		if (f2->isSet()) {
			FeatureTerm *f;
			List<FeatureTerm> *l=f2->set_values_quick();
			l->Rewind();
			while(l->Iterate(f)) v2.Add(f);
		} else {
			v2.Add(f2);
		} /* if */ 
	} /* if */ 

//	printf("[%i,%i]\n",v1.Length(),v2.Length());

	if (v2.Length()>v1.Length()) size=v2.Length();
						    else size=v1.Length();

	if (v2.Length()>0) assignments2b=new int[v2.Length()];
				  else assignments2b=0;

	max_size=v1.Length()+v2.Length();

	// Set max_size to 1 when the feature is NOT a relation
	if (singleton) max_size=1;

	for(;size<=max_size;size++) {
		bool more_mappings=true;

//		printf("Trying with set size %i\n",size);

		assignments1=new int[size];
		assignments2=new int[size];

		// The first set is mapped directly to the elemenst of the resulting set:
		for(i=0;i<v1.Length();i++) assignments1[i]=i;
		for(;i<size;i++) assignments1[i]=-1;

		// Start with the initial direct mapping, and iterate though all the possible mappings:
		for(i=0;i<v2.Length();i++) {
			assignments2[i]=i;
			assignments2b[i]=i;
		} //  if
		for(;i<size;i++) assignments2[i]=-1;
		
		do{
			// Test if the assignment is valid:
			{
				bool valid=true;

				// test1, each new element has at least one element assigned:
				if (valid) for(i=0;i<size && valid;i++) if (assignments1[i]==-1 || assignments2[i]==-1) valid=false;
				if (valid) {
					for(i=0;i<v2.Length() && valid;i++) {
						for(j=0;j<v2.Length() && valid;j++) {
							if (i!=j && assignments2b[i]==assignments2b[j]) valid=false;
						} /// for 
					} /// for 
				} /* if */ 

				if (valid) {
/*
					printf("S1 [ ");
					for(i=0;i<size;i++) printf("%i ",assignments1[i]);
					printf("]\n");

					printf("S2 [ ");
					for(i=0;i<size;i++) printf("%i ",assignments2[i]);
					printf("] from [ ");
					for(i=0;i<v2.Length();i++) printf("%i ",assignments2b[i]);
					printf("]\n");
*/

					// Unify each element of the set:
					lr=new List<UnificationResult>;
					initial_lr->Rewind();
					while(initial_lr->Iterate(r)) lr->Add(r->clone(domain_model));

					for(j=0;j<size;j++) {
						FeatureTerm *tmp1,*tmp2;

						lr3=new List<UnificationResult>;
						lr->Rewind();
						i=0;
						while(lr->Iterate(r)) {
//							printf("Considering new element %i (with bindings %i/%i)\n",j,i+1,lr->Length());
							i++;

							tmp1=0;
							if (assignments1[j]!=-1) tmp1=v1[assignments1[j]];
							tmp2=0;
							if (assignments2[j]!=-1) tmp2=v2[assignments2[j]];

							lr2=ft_internal_unification(tmp1,tmp2,&(r->m_bindings),&(r->m_stack),ontology,domain_model);
							if (lr2!=0) {
								while(!lr2->EmptyP()) {
									r2=lr2->ExtractIni();

									assert(!r2->m_u->isSet());

									// look for the proper clone of "r->m_u":
									{
										FeatureTerm *u;
										if (r2->m_stack[0]->getDataType()==3 ||
											r2->m_stack[0]->getDataType()==-1) delete r2->m_stack.ExtractIni();
										u=r2->m_stack[0];

										assert(u!=0);
										assert(u->isSet());
										u->addSetValue(r2->m_u);
										r2->m_u=new FeatureTerm(u);
									}

									lr3->Add(r2);
								} // while
								delete lr2;
							} /* if */ 
						} /* while */ 
						delete lr;
						lr=lr3;

					} // for 

					while(!lr->EmptyP()) {
						r=lr->ExtractIni();
						if (r->m_u->isSet() && r->m_u->set_values_quick()->Length()==1) {
							FeatureTerm *f=r->m_u;
							r->m_u=new FeatureTerm(r->m_u->set_values_quick()->operator [](0));
							delete f;
						} /* if */ 
						final_lr->Add(r);
					} // while
					delete lr;
					lr=0;

				} // if 
			}

			// generate the next mapping:
			if (assignments2b!=0) {
				bool end=false;

				i=v2.Length()-1;

				do{
					assignments2b[i]++;
					if (assignments2b[i]>=size) {
						assignments2b[i]=0;
						i--;
					} else {
						end=true;
					} /* if */ 
				}while(!end && i>=0);
				if (i<0) {
					more_mappings=false;
				} else {
					for(i=0;i<size;i++) assignments2[i]=-1;
					for(i=0;i<v2.Length();i++) assignments2[assignments2b[i]]=i;
				} // if
			} else {
				more_mappings=false;
			} // if

		}while(more_mappings);

		// ...

		delete []assignments1;
		delete []assignments2;
	} /* for */ 

	if (assignments2b!=0) delete []assignments2b;

	v1.ExtractAll();
	v2.ExtractAll();

	delete initial_lr;

	if (final_lr->EmptyP()) {
		delete final_lr;
		final_lr=0;
	} /* if */ 

//	printf("<set_internal_unification succeeded and returned %i results>\n",final_lr->Length());
	return final_lr;
} // set_internal_unification


FeatureTerm *integer_unification(FeatureTerm *f1,FeatureTerm *f2,FeatureTerm *u,Ontology *o)
{
	Sort *s=u->getSort();

	if (f1==0) {
		delete u;
		return f2->clone();
	} /* if */ 

	if (f2==0) {
		delete u;
		return f1->clone();
	} /* if */ 

	if (f1->specificIntValueP()) {
		/* specific value: */ 
		if (f2->specificIntValueP()) {
			/* specific value: */ 
			if (f2->getInt()!=f1->getInt()) {
				delete u;
				return 0;
			} // if 
			
			delete u;
			u=new FeatureTerm((Symbol *)0,f1->getInt(),o);
			u->setSort(s);
			return u;
		} else {
			/* undefined value: */ 
			delete u;
			u=new FeatureTerm((Symbol *)0,f1->getInt(),o);
			u->setSort(s);
			return u;
		} /* if */ 
	} else {
		/* undefined value: */ 
		if (f2->specificIntValueP()) {
			/* specific value: */ 
			delete u;
			u=new FeatureTerm((Symbol *)0,f2->getInt(),o);
			u->setSort(s);
			return u;
		} else {
			/* undefined value: */ 
			return u;
		} /* if */ 
	} /* if */ 

	delete u;
	return 0;
} /* integer_unification */ 



FeatureTerm *float_unification(FeatureTerm *f1,FeatureTerm *f2,FeatureTerm *u,Ontology *o)
{
	Sort *s=u->getSort();

	if (f1==0) {
		delete u;
		return f2->clone();
	} /* if */ 

	if (f2==0) {
		delete u;
		return f1->clone();
	} /* if */ 

	if (f1->specificFloatValueP()) {
		/* specific value: */ 
		if (f2->specificFloatValueP()) {
			/* specific value: */ 
			if (f2->getFloat()!=f1->getFloat()) {
				delete u;
				return 0;
			} // if 
						
			delete u;
			u=new FeatureTerm((Symbol *)0,f1->getFloat(),o);
			u->setSort(s);
			return u;
		} else {
			delete u;
			u=new FeatureTerm((Symbol *)0,f1->getFloat(),o);
			u->setSort(s);
			return u;
		} /* if */ 
	} else {
		/* undefined value: */ 
		if (f2->specificFloatValueP()) {
			delete u;
			u=new FeatureTerm((Symbol *)0,f2->getFloat(),o);
			u->setSort(s);
			return u;
		} else {
			return u;			
		} /* if */ 
	} /* if */ 

	delete u;
	return 0;
} /* float_unification */ 



